active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
F(mark(X)) → F(X)
MARK(a) → ACTIVE(a)
ACTIVE(f(f(a))) → G(f(a))
MARK(g(X)) → ACTIVE(g(X))
MARK(f(X)) → F(mark(X))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
G(active(X)) → G(X)
G(mark(X)) → G(X)
ACTIVE(f(f(a))) → F(g(f(a)))
F(active(X)) → F(X)
MARK(f(X)) → MARK(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(mark(X)) → F(X)
MARK(a) → ACTIVE(a)
ACTIVE(f(f(a))) → G(f(a))
MARK(g(X)) → ACTIVE(g(X))
MARK(f(X)) → F(mark(X))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
G(active(X)) → G(X)
G(mark(X)) → G(X)
ACTIVE(f(f(a))) → F(g(f(a)))
F(active(X)) → F(X)
MARK(f(X)) → MARK(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
G(active(X)) → G(X)
G(mark(X)) → G(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(active(X)) → G(X)
G(mark(X)) → G(X)
The value of delta used in the strict ordering is 16.
POL(active(x1)) = 4 + x_1
POL(mark(x1)) = 4 + (4)x_1
POL(G(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
F(mark(X)) → F(X)
F(active(X)) → F(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(mark(X)) → F(X)
F(active(X)) → F(X)
The value of delta used in the strict ordering is 16.
POL(active(x1)) = 4 + (4)x_1
POL(mark(x1)) = 4 + x_1
POL(F(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
MARK(f(X)) → MARK(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
MARK(f(X)) → MARK(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
The value of delta used in the strict ordering is 1/2.
POL(active(x1)) = x_1
POL(MARK(x1)) = 4 + (4)x_1
POL(f(x1)) = 1/4 + (4)x_1
POL(a) = 0
POL(g(x1)) = 0
POL(mark(x1)) = x_1
POL(ACTIVE(x1)) = 7/2 + (5/2)x_1
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(active(X)) → g(X)
g(mark(X)) → g(X)
mark(f(X)) → active(f(mark(X)))
active(f(f(a))) → mark(f(g(f(a))))
mark(a) → active(a)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)